S Ideal of R == S SubGrp of R+gp & (a, b:|R|. (S(a))  (S(a * b))) 

latex

---

clarification:

S Ideal of R == S SubGrp of R+gp & (a:|R|, b:|R|. (S(a))  (S(a (*R) b))) 

latex

Up	rings 1
Wellformedness Lemmas	ideal p wf
Definitions	P & Q, s SubGrp of g, r+gp, x:A. B(x), |r|, P  Q, x f y, *